$\forall$$A$:Type, $l$:($A$ List). ($\neg$($l$ = [])) $\Rightarrow$ ge($\parallel$$l$$\parallel$; 1)